(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a(x1) → b(x1)
b(b(b(c(x1)))) → a(c(c(b(a(a(x1))))))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → a(c(c(b(a(a(z0))))))
Tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(c(c(b(a(a(z0)))))), B(a(a(z0))), A(a(z0)), A(z0))
S tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(c(c(b(a(a(z0)))))), B(a(a(z0))), A(a(z0)), A(z0))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2
(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
B(
b(
b(
c(
z0)))) →
c2(
A(
c(
c(
b(
a(
a(
z0)))))),
B(
a(
a(
z0))),
A(
a(
z0)),
A(
z0)) by
B(b(b(c(x0)))) → c2(A(c(c(b(b(a(x0)))))), B(a(a(x0))), A(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(c(c(b(a(b(z0)))))), B(a(a(z0))), A(a(z0)), A(z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → a(c(c(b(a(a(z0))))))
Tuples:
A(z0) → c1(B(z0))
B(b(b(c(x0)))) → c2(A(c(c(b(b(a(x0)))))), B(a(a(x0))), A(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(c(c(b(a(b(z0)))))), B(a(a(z0))), A(a(z0)), A(z0))
S tuples:
A(z0) → c1(B(z0))
B(b(b(c(x0)))) → c2(A(c(c(b(b(a(x0)))))), B(a(a(x0))), A(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(c(c(b(a(b(z0)))))), B(a(a(z0))), A(a(z0)), A(z0))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2
(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
B(
b(
b(
c(
x0)))) →
c2(
A(
c(
c(
b(
b(
a(
x0)))))),
B(
a(
a(
x0))),
A(
a(
x0)),
A(
x0)) by
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → a(c(c(b(a(a(z0))))))
Tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(c(c(b(a(b(z0)))))), B(a(a(z0))), A(a(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)))
S tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(c(c(b(a(b(z0)))))), B(a(a(z0))), A(a(z0)), A(z0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2, c2
(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
B(
b(
b(
c(
z0)))) →
c2(
A(
c(
c(
b(
a(
b(
z0)))))),
B(
a(
a(
z0))),
A(
a(
z0)),
A(
z0)) by
B(b(b(c(x0)))) → c2(A(c(c(b(b(b(x0)))))), B(a(a(x0))), A(a(x0)), A(x0))
B(b(b(c(b(b(c(z0))))))) → c2(A(c(c(b(a(a(c(c(b(a(a(z0))))))))))), B(a(a(b(b(c(z0)))))), A(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)), A(x0))
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → a(c(c(b(a(a(z0))))))
Tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)))
B(b(b(c(b(b(c(z0))))))) → c2(A(c(c(b(a(a(c(c(b(a(a(z0))))))))))), B(a(a(b(b(c(z0)))))), A(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)), A(x0))
S tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)))
B(b(b(c(b(b(c(z0))))))) → c2(A(c(c(b(a(a(c(c(b(a(a(z0))))))))))), B(a(a(b(b(c(z0)))))), A(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)), A(x0))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2, c2, c2
(9) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(a(z0)), A(z0)) by B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(b(z0)), A(z0))
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → a(c(c(b(a(a(z0))))))
Tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(a(z0)), A(z0))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)))
B(b(b(c(b(b(c(z0))))))) → c2(A(c(c(b(a(a(c(c(b(a(a(z0))))))))))), B(a(a(b(b(c(z0)))))), A(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(b(z0)), A(z0))
S tuples:
A(z0) → c1(B(z0))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)))
B(b(b(c(b(b(c(z0))))))) → c2(A(c(c(b(a(a(c(c(b(a(a(z0))))))))))), B(a(a(b(b(c(z0)))))), A(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(b(z0)), A(z0))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2, c2, c2
(11) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0))) by B(b(b(c(z0)))) → c2(B(a(a(z0))), A(b(z0)))
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → a(c(c(b(a(a(z0))))))
Tuples:
A(z0) → c1(B(z0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(a(z0)), A(z0))
B(b(b(c(b(b(c(z0))))))) → c2(A(c(c(b(a(a(c(c(b(a(a(z0))))))))))), B(a(a(b(b(c(z0)))))), A(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(B(a(a(z0))), A(b(z0)))
S tuples:
A(z0) → c1(B(z0))
B(b(b(c(b(b(c(z0))))))) → c2(A(c(c(b(a(a(c(c(b(a(a(z0))))))))))), B(a(a(b(b(c(z0)))))), A(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(B(a(a(z0))), A(b(z0)))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2, c2, c2
(13) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace B(b(b(c(x0)))) → c2(A(c(c(b(b(b(x0)))))), B(a(a(x0))), A(a(x0)), A(x0)) by B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(b(z0)), A(z0))
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → a(c(c(b(a(a(z0))))))
Tuples:
A(z0) → c1(B(z0))
B(b(b(c(b(b(c(z0))))))) → c2(A(c(c(b(a(a(c(c(b(a(a(z0))))))))))), B(a(a(b(b(c(z0)))))), A(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(B(a(a(z0))), A(b(z0)))
S tuples:
A(z0) → c1(B(z0))
B(b(b(c(b(b(c(z0))))))) → c2(A(c(c(b(a(a(c(c(b(a(a(z0))))))))))), B(a(a(b(b(c(z0)))))), A(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(B(a(a(z0))), A(b(z0)))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2, c2, c2
(15) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
A(
z0) →
c1(
B(
z0)) by
A(b(b(c(b(b(c(y0))))))) → c1(B(b(b(c(b(b(c(y0))))))))
A(b(b(c(y0)))) → c1(B(b(b(c(y0)))))
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → a(c(c(b(a(a(z0))))))
Tuples:
B(b(b(c(b(b(c(z0))))))) → c2(A(c(c(b(a(a(c(c(b(a(a(z0))))))))))), B(a(a(b(b(c(z0)))))), A(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(B(a(a(z0))), A(b(z0)))
A(b(b(c(b(b(c(y0))))))) → c1(B(b(b(c(b(b(c(y0))))))))
A(b(b(c(y0)))) → c1(B(b(b(c(y0)))))
S tuples:
B(b(b(c(b(b(c(z0))))))) → c2(A(c(c(b(a(a(c(c(b(a(a(z0))))))))))), B(a(a(b(b(c(z0)))))), A(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(B(a(a(z0))), A(b(z0)))
A(b(b(c(b(b(c(y0))))))) → c1(B(b(b(c(b(b(c(y0))))))))
A(b(b(c(y0)))) → c1(B(b(b(c(y0)))))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
B, A
Compound Symbols:
c2, c2, c2, c1
(17) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
B(b(b(c(b(b(c(z0))))))) → c2(A(c(c(b(a(a(c(c(b(a(a(z0))))))))))), B(a(a(b(b(c(z0)))))), A(a(b(b(c(z0))))), A(b(b(c(z0)))))
B(b(b(c(x0)))) → c2(B(a(a(x0))), A(a(x0)), A(x0))
B(b(b(c(z0)))) → c2(A(c(c(b(b(b(z0)))))), B(a(a(z0))), A(b(z0)), A(z0))
B(b(b(c(z0)))) → c2(B(a(a(z0))), A(b(z0)))
A(b(b(c(b(b(c(y0))))))) → c1(B(b(b(c(b(b(c(y0))))))))
A(b(b(c(y0)))) → c1(B(b(b(c(y0)))))
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(z0) → b(z0)
b(b(b(c(z0)))) → a(c(c(b(a(a(z0))))))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:none
Compound Symbols:none
(19) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(20) BOUNDS(O(1), O(1))